perm filename ENERGY.XGP[F84,JMC] blob sn#780109 filedate 1984-12-13 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓CS206␈↓ ¬TFINAL EXAMINATION␈↓ 
lFALL 1984 

␈↓ α∧␈↓␈↓ αTThis␈α
examination␈α
is␈α
open␈α∞book␈α
and␈α
notes.␈α
 Write␈α∞LISP␈α
functions␈α
or␈α
predicates␈α∞and␈α
make
␈↓ α∧␈↓proofs␈αas␈αfollows␈α
except␈αwhere␈αsomething␈α
else␈αis␈αrequested.␈α
 Either␈αnotation␈αmay␈α
be␈αused.␈α Be␈α
sure
␈↓ α∧␈↓to␈α
indicate␈α
in␈α
an␈α
emphatic␈α
way␈α
the␈α
logical␈αsentences␈α
indicating␈α
what␈α
is␈α
to␈α
be␈α
proved␈α
and␈α
the␈α␈↓	F␈↓'s␈α
of
␈↓ α∧␈↓any␈αinductions␈α
that␈αneed␈α
to␈αbe␈αmade.␈α
 You␈αmay␈α
assume␈αthat␈αyour␈α
functions␈αare␈α
total␈αbut␈α
will␈αbe
␈↓ α∧␈↓suitably penalized if they aren't.

␈↓ α∧␈↓1.␈α∞␈↓↓eqshape[x,y]␈↓␈α∞is␈α∞true␈α
if␈α∞the␈α∞S-expressions␈α∞␈↓↓x␈↓␈α
and␈α∞␈↓↓y␈↓␈α∞have␈α∞the␈α
same␈α∞shape,␈α∞i.e.␈α∞the␈α∞same␈α
car-cdr
␈↓ α∧␈↓chains reach atoms in the two expressions.  5 points

␈↓ α∧␈↓2.␈αProve␈αthat␈α␈↓↓eqshape␈↓␈αis␈αan␈αequivalence␈αrelation,␈αi.e.␈αprove␈α␈↓↓∀x.eqshape(x,x)␈↓␈αand␈α␈↓↓∀x␈αy.eqshape(x,y)
␈↓ α∧␈↓↓⊃ eqshape(y,x)␈↓ and ␈↓↓∀x y z.eqshape(x,y) ∧ eqshape(y,z) ⊃ eqshape(x,z)␈↓.  15 points.

␈↓ α∧␈↓3.␈α
␈↓↓shapes␈α
n␈↓␈αis␈α
a␈α
list␈α
of␈αthe␈α
distinct␈α
shapes␈α
that␈αhave␈α
␈↓↓n␈↓␈α
atoms.␈α
Each␈αshape␈α
is␈α
represented␈α
by␈αa␈α
single
␈↓ α∧␈↓S-expression of that shape each of whose atoms is A.  Thus

␈↓ α∧␈↓␈↓↓shapes␈↓ 4 = ((A.(A.(A.A))) (A.((A.A).A)) ((A.A).(A.A)) ((A.(A.A)).A) (((A.A).A).A))).

␈↓ α∧␈↓I␈α∞have␈α∞left␈α∂out␈α∞the␈α∞spaces␈α∂that␈α∞Common␈α∞Lisp␈α∂would␈α∞want␈α∞and␈α∂produce␈α∞in␈α∞the␈α∂example.␈α∞ Don't
␈↓ α∧␈↓worry about it. 15 points.

␈↓ α∧␈↓4.␈α
Write␈α
a␈α
logical␈α
formula␈αthat␈α
expresses␈α
the␈α
correctness␈α
of␈αthe␈α
function␈α
␈↓↓shapes␈↓.␈α
 Don't␈α
try␈αto␈α
prove
␈↓ α∧␈↓it. 15 points.

␈↓ α∧␈↓5.␈α
A␈α
queue␈α
may␈α
be␈α
represented␈αby␈α
␈↓↓cons␈↓␈α
cell␈α
whose␈α
␈↓αa␈↓-part␈α
points␈αto␈α
a␈α
list␈α
of␈α
the␈α
members␈α
of␈αthe
␈↓ α∧␈↓queue␈αand␈αwhose␈α␈↓αd␈↓-part␈αpoints␈αto␈αthe␈αlast␈αword␈αof␈αthe␈αlist.␈α Such␈αa␈αqueue␈αis␈αshown␈αin␈αthe␈αfigure.
␈↓ α∧␈↓The␈αdirty␈αLisp␈αfunction␈α␈↓↓insert[x,q]␈↓␈αreturns␈αa␈αqueue␈αthat␈αhas␈αhad␈α␈↓↓x␈↓␈αinserted␈αas␈αthe␈αlast␈αelement␈αof
␈↓ α∧␈↓the␈α
queue␈α␈↓↓q.␈↓␈α
The␈α
dirty␈αLisp␈α
function␈α␈↓↓remove␈α
q␈↓␈α
returns␈αa␈α
list␈αwhose␈α
sole␈α
element␈αis␈α
the␈αfirst␈α
element
␈↓ α∧␈↓of␈αthe␈α
queue␈α␈↓↓q␈↓␈α
and␈αas␈αa␈α
side␈αeffect␈α
removes␈αthe␈α
element␈αfrom␈αthe␈α
queue.␈α If␈α
the␈αqueue␈α
is␈αempty,
␈↓ α∧␈↓␈↓↓remove q =␈↓ NIL.  20 points.
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓6.␈α␈↓↓l-rotate␈αx␈↓␈αis␈αthe␈αresult␈αof␈αrotating␈αthe␈αS-expression␈α␈↓↓x␈↓␈αto␈αthe␈αleft␈αpreserving␈αthe␈αshape.␈α Thus␈α␈↓↓l-
␈↓ α∧␈↓↓rotate␈↓ (A . (B . C)) = (B . (C . A)).␈α
 Similarly␈α
␈↓↓r-rotate␈αx␈↓␈α
is␈α
the␈αresult␈α
of␈α
rotating␈α␈↓↓x␈↓␈α
to␈α
the␈αright.␈α
 The
␈↓ α∧␈↓program should be in pure Lisp, i.e. shouldn't modify the existing structure.

␈↓ α∧␈↓Hint:␈α
l-rotate␈α∞and␈α
r-rotate␈α∞are␈α
analogous␈α
to␈α∞the␈α
lcyle␈α∞and␈α
rcycle␈α
that␈α∞operate␈α
on␈α∞lists.␈α
 However,
␈↓ α∧␈↓using␈αthis␈αanalogy␈αrequires␈αrather␈αfancy␈αanalogues␈αof␈α␈↓αa␈↓,␈α␈↓αd␈↓␈αand␈α␈↓↓cons.␈↓␈αThis␈αproblem␈αmay␈αbe␈αfairly
␈↓ α∧␈↓difficult.  15 points.

␈↓ α∧␈↓7.␈α
Sketch␈α
a␈α
proof␈α
that␈α
␈↓↓∀x.␈α
l-rotate␈α
r-rotate␈α
x␈α
=␈α
x␈↓.␈α
 For␈α
any␈α
propositions␈α
to␈α
be␈α
proved␈αby␈α
induction,
␈↓ α∧␈↓show the induction statement.  15 points.